\relax 
\citation{a15,indusREV}
\citation{daghsen2010applying}
\citation{giese2010model}
\@writefile{toc}{\contentsline {title}{Automated Verification of Model Transformations in the Automotive Industry\unskip {}}{1}}
\@writefile{toc}{\authcount {5}}
\@writefile{toc}{\contentsline {author}{Gehan M. K. Selim\unskip {} \and Fabian B\"uttner\unskip {} \and James R. Cordy\unskip {} \and Juergen Dingel\unskip {} \and Shige Wang\unskip {} }{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\newlabel{sec:intro}{{1}{1}}
\citation{Jouault2008ATL}
\citation{ECMFApaper}
\citation{Buettner2012ICFEM}
\citation{ECMFApaper}
\citation{ECMFApaper}
\citation{autosar}
\@writefile{toc}{\contentsline {section}{\numberline {2}Background: Model Transformation in the Automotive Industry}{2}}
\newlabel{sec:MT_AutomotiveIndustry}{{2}{2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Overview of the Model Transformation Problem}{2}}
\newlabel{subsec:Overview_MT_Problem}{{2.1}{2}}
\citation{ECMFApaper}
\citation{ECMFApaper}
\citation{ECMFApaper}
\citation{systemp}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}The GM Metamodel}{3}}
\newlabel{subsec:TheGMmm}{{2.2}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Subset of the GM metamodel directly used by our transformation in\nobreakspace  {}\cite  {ECMFApaper}.}}{3}}
\newlabel{fig:gmMMfig}{{1}{3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}The AUTOSAR Metamodel}{3}}
\newlabel{TheAUTOSARmm}{{2.3}{3}}
\citation{Buettner2012ICFEM}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Subset of the AUTOSAR System Template directly used by our transformation.}}{4}}
\newlabel{fig:systempfig}{{2}{4}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Verification Methodology}{4}}
\newlabel{sec:FormalVer_ConstSolvers}{{3}{4}}
\citation{Kuhlmann2011}
\citation{USE}
\citation{Torlak2007Kodkod}
\newlabel{eqn:unsatform}{{2}{5}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Transformation model example}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(a)}{\ignorespaces {Source MM}}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(b)}{\ignorespaces {Target MM}}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(c)}{\ignorespaces {\relax ATL transformation}}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(d)}{\ignorespaces b}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(e)}{\ignorespaces {\relax OCL constraints for ATL semantics (excerpt)}}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(f)}{\ignorespaces {\relax Preconditions}}}{5}}
\@writefile{lof}{\contentsline {subfigure}{\numberline{(g)}{\ignorespaces {\relax Postconditions}}}{5}}
\newlabel{fig:tmexample}{{3}{5}}
\citation{Buettner2012ICFEM}
\citation{Tisi2009HOT}
\citation{ECMFApaper}
\citation{ECMFApaper}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces The tool chain used to perform the transformation verification.}}{6}}
\newlabel{fig:toolchain}{{4}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Case Study: Evaluating Transformations in the Automotive Industry Using Automated Verification}{6}}
\newlabel{sec:caseStudy}{{4}{6}}
\citation{ECMFApaper}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Reimplementation of the GM-to-AUTOSAR Model Transformation}{7}}
\newlabel{subsec:reimplementationMT}{{4.1}{7}}
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces The types of ATL constructs used to reimplement the transformation, their designated names, and their input and output element types.}}{7}}
\newlabel{tab:rulesUsedinMT}{{1}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Formulation of OCL Pre- and Postconditions}{7}}
\newlabel{subsec:FormulationOCLConsts}{{4.2}{7}}
\@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Formulated OCL Constraints}}{8}}
\newlabel{tab:OCLConsts}{{2}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Counterexample generated for the mult. inv. $\mathtt  {CompositionType\_component}$.}}{10}}
\newlabel{fig:ctrex}{{5}{10}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Results}{10}}
\newlabel{sec:results}{{5}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Verifying the Formulated OCL Constraints}{10}}
\newlabel{subsec:VerifFormOCLConsts}{{5.1}{10}}
\@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces The two rules that required updates to address the two violations of multiplicity invariants.}}{11}}
\newlabel{tab:buggyRules}{{3}{11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Performance of the Verification Approach}{11}}
\newlabel{subsec:Scalability}{{5.2}{11}}
\citation{Torlak2007Kodkod}
\citation{Jacobs01}
\@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Translation\textbackslash Constraint Solving times (seconds) for the 18 constraints on different scopes. For a scope of 12, the verification of S1 did not terminate in a week.}}{12}}
\newlabel{tab:scalres}{{4}{12}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Discussion}{12}}
\newlabel{sec:discussion}{{6}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Strengths of the Verification Approach}{12}}
\newlabel{subsec:strengthPropApp}{{6.1}{12}}
\citation{ZOO}
\citation{Buettner2012MoDELS}
\citation{Buettner2012MoDELS}
\citation{Sen2009b}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.2}Limitations of the Verification Approach}{13}}
\newlabel{subsec:threatsToValidity}{{6.2}{13}}
\citation{ANAS}
\citation{Baresi2006}
\citation{Inaba2011}
\citation{Troya2011ATL}
\citation{Cabot2010}
\citation{Buettner2012ICFEM}
\citation{Buettner2012MoDELS}
\citation{DEDU}
\citation{LEVI}
\citation{Rensink2008}
\citation{REFC}
\citation{VQVT}
\citation{Guerra2013}
\citation{GOGO}
\citation{Braga2011}
\citation{Cariou2009}
\citation{CRSP}
\citation{Kuhlmann2011}
\citation{Gonzalez2012}
\citation{Queralt2012}
\citation{Brucker2009}
\citation{Jackson2013}
\@writefile{toc}{\contentsline {section}{\numberline {7}Related Work}{14}}
\newlabel{sec:RelatedWork}{{7}{14}}
\citation{ECMFApaper}
\@writefile{toc}{\contentsline {section}{\numberline {8}Conclusion and Future Work}{15}}
\newlabel{sec:concFW}{{8}{15}}
\bibstyle{abbrv}
\bibdata{MODELS_bib}
\bibcite{systemp}{1}
\bibcite{autosar}{2}
\bibcite{ANAS}{3}
\bibcite{DEDU}{4}
\bibcite{Baresi2006}{5}
\bibcite{REFC}{6}
\bibcite{Braga2011}{7}
\bibcite{Brucker2009}{8}
\bibcite{Buettner2012MoDELS}{9}
\bibcite{Buettner2012ICFEM}{10}
\bibcite{Cabot2010}{11}
\bibcite{Cariou2009}{12}
\bibcite{a15}{13}
\bibcite{daghsen2010applying}{14}
\bibcite{giese2010model}{15}
\bibcite{GOGO}{16}
\bibcite{Gonzalez2012}{17}
\bibcite{Guerra2013}{18}
\bibcite{Inaba2011}{19}
\bibcite{Jackson2013}{20}
\bibcite{Jacobs01}{21}
\bibcite{Jouault2008ATL}{22}
\bibcite{Kuhlmann2011}{23}
\bibcite{LEVI}{24}
\bibcite{indusREV}{25}
\bibcite{CRSP}{26}
\bibcite{Queralt2012}{27}
\bibcite{Rensink2008}{28}
\bibcite{ECMFApaper}{29}
\bibcite{Sen2009b}{30}
\bibcite{VQVT}{31}
\bibcite{Tisi2009HOT}{32}
\bibcite{Torlak2007Kodkod}{33}
\bibcite{Troya2011ATL}{34}
\bibcite{USE}{35}
\bibcite{ZOO}{36}
